M.rframe(A.pre p for a)
== xdom((M.2.2.2.2.2.2.2.2.2.2).1). 

== L=(M.2.2.2.2.2.2.2.2.2.2).1(x)  
== L(deq-member(KindDeq;locl(a);L))  (s1, s2:A.state. (s1  s2 mod x)  (p(s1) = p(s2))) 

latex

---

clarification:

M.rframe(A.pre p for a)
== IdIdDeqxdom((M.2.2.2.2.2.2.2.2.2.2).1). 

== L=(M.2.2.2.2.2.2.2.2.2.2).1(x)  
== L(deq-member(KindDeq;locl(a);L))
==  (s1:A.state, s2:A.state. ma-x-equiv(A;x;s1;s2)  (p(s1) = p(s2)  )) 

latex

Definitions	xdom(f). v=f(x)   P(x;v), Id, IdDeq, t.1, t.2, P  Q, b, deq-member(eq;x;L), KindDeq, locl(a), x:A. B(x), M.state, P  Q, (s1  s2 mod x), s = t, , f(a)
FDL editor aliases	ma-rframe-pre